-------------------------- MODULE TransitiveClosure -------------------------
(***************************************************************************)
(* Mathematicians define a relation R to be a set of ordered pairs, and    *)
(* write `s R t' to mean `<<s, t>> \in R'.  The transitive closure TC(R)   *)
(* of the relation R is the smallest relation containing R such that,        *)
(* `s TC(R) t' and `t TC(R) u' imply `s TC(R) u', for any s, t, and u.     *)
(* This module shows several ways of defining the operator TC.             *)
(*                                                                         *)
(* It is sometimes more convenient to represent a relation as a            *)
(* Boolean-valued function of two arguments, where `s R t' means R[s, t].  *)
(* It is a straightforward exercise to translate everything in this module *)
(* to that representation.                                                 *)
(*                                                                         *)
(* Mathematicians say that R is a relation on a set S iff R is a subset of *)
(* S \X S.  Let the `support' of a relation R be the set of all elements s *)
(* such that `s R t' or `t R s' for some t.  Then any relation is a        *)
(* relation on its support.  Moreover, the support of R is the support of  *)
(* TC(R).  So, to define the transitive closure of R, there's no need to   *)
(* say what set R is a relation on.                                        *)
(*                                                                         *)
(* Let's begin by importing some modules we'll need and defining the the   *)
(* support of a relation.                                                  *)
(***************************************************************************)
EXTENDS Integers, Sequences, FiniteSets, TLC

Support(R) == {r[1] : r \in R} \cup {r[2] : r \in R}

(***************************************************************************)
(* A relation R defines a directed graph on its support, where there is an *)
(* edge from s to t iff `s R t'.  We can define TC(R) to be the relation   *)
(* such that `s R t' holds iff there is a path from s to t in this graph.  *)
(* We represent a path by the sequence of nodes on the path, so the length *)
(* of the path (the number of edges) is one greater than the length of the *)
(* sequence.  We then get the following definition of TC.                  *)
(***************************************************************************)
TC(R) == 
  LET S == Support(R)     
  IN  {<<s, t>> \in S \X S :
        \E p \in Seq(S) : /\ Len(p) > 1
                          /\ p[1] = s
                          /\ p[Len(p)] = t
                          /\ \A i \in  1..(Len(p)-1) : <<p[i], p[i+1]>> \in R}

(***************************************************************************)
(* This definition can't be evaluated by TLC because Seq(S) is an infinite *)
(* set.  However, it's not hard to see that if R is a finite set, then it  *)
(* suffices to consider paths whose length is at most Cardinality(S).      *)
(* Modifying the definition of TC we get the following definition that     *)
(* defines TC1(R) to be the transitive closure of R, if R is a finite set. *)
(* The LET expression defines BoundedSeq(S, n) to be the set of all        *)
(* sequences in Seq(S) of length at most n.                                *)
(***************************************************************************)
TC1(R) == 
  LET BoundedSeq(S, n) == UNION {[1..i -> S] : i \in 0..n}
      S == Support(R)     
  IN  {<<s, t>> \in S \X S :
                    \E p \in BoundedSeq(S, Cardinality(S)+1) : 
                            /\ Len(p) > 1
                            /\ p[1] = s
                            /\ p[Len(p)] = t
                            /\ \A i \in  1..(Len(p)-1) : <<p[i], p[i+1]>> \in R}

(***************************************************************************)
(* This naive method used by TLC to evaluate expressions makes this        *)
(* definition rather inefficient.  (As an exercise, find an upper bound on *)
(* its complexity.) To obtain a definition that TLC can evaluate more      *)
(* efficiently, let's look at the closure operation more algebraically.    *)
(* Let's define the composition of two relations R and T as follows.       *)
(***************************************************************************)
R ** T == LET SR == Support(R)
              ST == Support(T)
          IN  {<<r, t>> \in SR \X ST : 
                \E s \in SR \cap ST : (<<r, s>> \in R) /\ (<<s, t>> \in T)}
                                         
(***************************************************************************)
(* We can then define the closure of R to equal                            *)
(*                                                                         *)
(*    R \cup (R ** R) \cup (R ** R ** R) \cup ...                          *)
(*                                                                         *)
(* For R finite, this union converges to the transitive closure when the   *)
(* number of terms equals the cardinality of the support of R.  This leads *)
(* to the following definition.                                            *)
(***************************************************************************)
TC2(R) ==
  LET C[n \in Nat] == IF n = 0 THEN R
                               ELSE C[n-1] \cup (C[n-1] ** R)
  IN  IF R = {} THEN {} ELSE C[Cardinality(Support(R)) - 1] 

(***************************************************************************)
(* These definitions of TC1 and TC2 are somewhat unsatisfactory because of *)
(* their use of Cardinality(S).  For example, it would be easy to make a   *)
(* mistake and use Cardinality(S) instead of Cardinality(S)+1 in the       *)
(* definition of TC1(R).  I find the following definition more elegant     *)
(* than the preceding two.  It is also more asymptotically more efficient  *)
(* because it makes O(log Cardinality (S)) rather than O(Cardinality(S))   *)
(* recursive calls.                                                        *)
(***************************************************************************)
RECURSIVE TC3(_)
TC3(R) == LET RR == R ** R
          IN  IF RR \subseteq R THEN R ELSE TC3(R \cup RR)

(***************************************************************************)
(* The preceding two definitions can be made slightly more efficient to    *)
(* execute by expanding the definition of ** and making some simple        *)
(* optimizations.  But, this is unlikely to be worth complicating the      *)
(* definitions for.                                                        *)
(*                                                                         *)
(* The following definition is (asymptotically) the most efficient.  It is *)
(* essentially the TLA+ representation of Warshall's algorithm.            *)
(* (Warshall's algorithm is typically written as an iterative procedure    *)
(* for the case of a relation on a set i..j of integers, when the relation *)
(* is represented as a Boolean-valued function.)                           *)
(***************************************************************************)
TC4(R) ==
  LET S == Support(R)
      RECURSIVE TCR(_)
      TCR(T) == IF T = {} 
                  THEN R
                  ELSE LET r == CHOOSE s \in T : TRUE
                           RR == TCR(T \ {r})
                       IN  RR \cup {<<s, t>> \in S \X S : 
                                      <<s, r>> \in RR /\ <<r, t>> \in RR}
  IN  TCR(S)
  
(***************************************************************************)
(* We now test that these four definitions are equivalent.  Since it's     *)
(* unlikely that all four are wrong in the same way, their equivalence     *)
(* makes it highly probable that they're correct.                          *)
(***************************************************************************)
ASSUME \A N \in 0..3 : 
          \A R \in SUBSET ((1..N) \X (1..N)) : /\ TC1(R) = TC2(R)
                                               /\ TC2(R) = TC3(R) 
                                               /\ TC3(R) = TC4(R)

(***************************************************************************)
(* Sometimes we want to represent a relation as a Boolean-valued operator, *)
(* so we can write `s R t' as R(s, t).  This representation is less        *)
(* convenient for manipulating relations, since an operator is not an      *)
(* ordinary value the way a function is.  For example, since TLA+ does not *)
(* permit us to define operator-valued operators, we cannot define a       *)
(* transitive closure operator TC so TC(R) is the operator that represents *)
(* the transitive closure.  Moreover, an operator R by itself cannot       *)
(* represent a relation; we also have to know what set it is an operator   *)
(* on.  (If R is a function, its domain tells us that.)                    *)
(*                                                                         *)
(* However, there may be situations in which you want to represent         *)
(* relations by operators.  In that case, you can define an operator TC so *)
(* that, if R is an operator representing a relation on S, and TCR is the  *)
(* operator representing it transitive closure, then                       *)
(*                                                                         *)
(*   TCR(s, t) = TC(R, S, s, t)                                            *)
(*                                                                         *)
(* for all s, t.  Here is the definition.  (This assumes that for an       *)
(* operator R on a set S, R(s, t) equals FALSE for all s and t not in S.)  *)
(***************************************************************************)
TC5(R(_,_), S, s, t) ==
  LET CR[n \in Nat, v \in S] == 
          IF n = 0 THEN R(s, v)
                   ELSE \/ CR[n-1, v] 
                        \/ \E u \in S : CR[n-1, u] /\ R(u, v)
  IN  /\ s \in S
      /\ t \in S
      /\ CR[Cardinality(S)-1, t]

(***************************************************************************)
(* Finally, the following assumption checks that our definition TC5 agrees *)
(* with our definition TC1.                                                *)
(***************************************************************************)
ASSUME \A N \in 0..3 : \A R \in SUBSET ((1..N) \X (1..N)) :
         LET RR(s, t) == <<s, t>> \in R
             S == Support(R)
         IN  \A s, t \in S : 
                TC5(RR, S, s, t) <=> (<<s, t>> \in TC1(R))
=============================================================================
